<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>The conversion tactic mode</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  
<h1 id="the-conversion-tactic-mode" class="markdown-heading">The conversion tactic mode <a class="hover-link" href="#the-conversion-tactic-mode">#</a></h1>
<p>Inside a tactic block, one can use the keyword <code>conv</code> to enter conversion
mode. This mode allows to travel inside assumptions and goals, even
inside <code>λ</code> binders in them, to apply rewriting or simplifying steps.</p>
<p>This is similar to the conversion tacticals (tactic combinators) found in
other theorem provers like HOL4, HOL Light or Isabelle.</p>
<h2 id="basic-navigation-and-rewriting" class="markdown-heading">Basic navigation and rewriting <a class="hover-link" href="#basic-navigation-and-rewriting">#</a></h2>
<p>As a first example, let us prove
<code>example (a b c : ℕ) : a * (b * c) = a * (c * b)</code> (examples in this file
are somewhat artificial since the <code>ring</code> tactic from
<code>tactic.ring</code> could finish them immediately). The naive first attempt is
to enter tactic mode and try <code>rw mul_comm</code>. But this transforms the goal
into <code>b * c * a = a * (c * b)</code>, after commuting the very first
multiplication appearing in the term. There are several ways to fix this
issue, and one way is to use a more precise tool : the
conversion mode.  The following code block shows the current target after
each line. Note that the target is prefixed by <code>|</code> where normal mode
shows a goal prefixed by <code>⊢</code> (these targets are still called &quot;goals&quot;
though).</p>
<pre><code class="language-lean">example (a b c : ℕ) : a * (b * c) = a * (c * b) :=
begin
  conv
  begin          -- | a * (b * c) = a * (c * b)
    to_lhs,      -- | a * (b * c)
    congr,       -- 2 goals : | a and | b * c
    skip,        -- | b * c
    rw mul_comm, -- | c * b
  end
end
</code></pre>
<p>The above snippet show three navigation commands:</p>
<ul>
<li><code>to_lhs</code> navigates to the left hand side of a relation (here
equality), there is also a <code>to_rhs</code> navigating to the right hand side.</li>
<li><code>congr</code> creates as many targets as there are arguments to the current
head function (here the head function is multiplication)</li>
<li><code>skip</code> goes to the next target</li>
</ul>
<p>Once arrived at the relevant target, we can use <code>rw</code> as in normal mode.
Note that Lean tries to solves the current goal if it became <code>x = x</code> (in
the strict syntactical sense, definitional equality is not enough: one
needs to conclude by <code>refl</code> or <code>trivial</code> in this case).</p>
<p>The second main reason to use conversion mode is to rewrite under
binders. Suppose we want to prove <code>example (λ x : ℕ, 0+x) = (λ x, x)</code>.
The naive first attempt is to enter tactic mode and try <code>rw zero_add</code>.
But this fails with a frustrating</p>
<pre><code>rewrite tactic failed, did not find
instance of the pattern in the target expression 0 + ?m_3
state:
⊢ (λ (x : ℕ), 0 + x) = λ (x : ℕ), x
</code></pre>
<p>The solution is:</p>
<pre><code class="language-lean">example : (λ x : ℕ, 0 + x) = (λ x, x) :=
begin
  conv
  begin           -- | (λ (x : ℕ), 0 + x) = λ (x : ℕ), x
    to_lhs,       -- | λ (x : ℕ), 0 + x
    funext,       -- | 0 + x
    rw zero_add,  -- | x
  end
end
</code></pre>
<p>where <code>funext</code> is the navigation command entering inside the <code>λ</code> binder.
Note that this example is somewhat artificial, one could also do:</p>
<pre><code class="language-lean">example : (λ x : ℕ, 0+x) = (λ x, x) :=
by funext ; rw zero_add
</code></pre>
<p>All this is also available to rewrite an hypothesis <code>H</code> from the local context
using <code>conv at H</code>.</p>
<h2 id="pattern-matching" class="markdown-heading">Pattern matching <a class="hover-link" href="#pattern-matching">#</a></h2>
<p>Navigation using the above commands can be tedious. One can shortcut it
using pattern matching as follows:</p>
<pre><code class="language-lean">example (a b c : ℕ) : a * (b * c) = a * (c * b) :=
begin
conv in (b*c)
begin          -- | b * c
  rw mul_comm, -- | c * b
end
end
</code></pre>
<p>As usual, <code>begin</code> and <code>end</code> can be replaced by curly brackets to
delimit conversion mode and a single tactic invocation can be introduced
by <code>by</code> to get the one liner:</p>
<pre><code class="language-lean">example (a b c : ℕ) : a * (b * c) = a * (c * b) :=
by conv in (b*c) { rw mul_comm }
</code></pre>
<p>Beware that a well known bug makes Lean printing: &quot;find converter
failed, pattern was not found&quot; when the tactics inside conversion mode
fail, even if the pattern was actually found.</p>
<p>Of course wild-cards are allowed:</p>
<pre><code class="language-lean">example (a b c : ℕ) : a + (b * c) = a + (c * b) :=
by conv in (_ * c) { rw mul_comm }
</code></pre>
<p>In all those cases, only the first match is affected.
A more sophisticated version of pattern matching is available inside
conversion mode using the <code>for</code> command. The following performs rewriting
only for the second and third occurrences of <code>b * c</code>:</p>
<pre><code class="language-lean">example (a b c : ℕ) : (b * c) * (b * c) * (b * c) = (b * c) * (c * b)  * (c * b):=
by conv { for (b * c) [2, 3] { rw mul_comm } }
</code></pre>
<h2 id="other-tactics-inside-conversion-mode" class="markdown-heading">Other tactics inside conversion mode <a class="hover-link" href="#other-tactics-inside-conversion-mode">#</a></h2>
<p>Besides rewriting using <code>rw</code>, one can use <code>simp</code>, <code>dsimp</code>, <code>change</code> and <code>whnf</code>.
<code>change</code> is a useful tool -- it allows changing a term to something
definitionally equal, rather like the <code>show</code> command in tactic mode.
The <code>whnf</code> command means &quot;reduces to weak head normal form&quot; and will eventually
be explained in <a href="https://leanprover.github.io/programming_in_lean/#08_Writing_Tactics.html">Programming in Lean</a> section 8.4.</p>
<p>Extensions to <code>conv</code> provided by mathlib, such as <code>ring</code> and <code>norm_num</code>, can be
found in the <a href="https://leanprover-community.github.io/mathlib_docs/tactics.html#conv">mathlib docs</a>.</p>

  </div>
</div>

  <nav class="footer navbar navbar-expand-lg navbar-light bg-light justify-content-end">
  <ul class="nav">
    <li class="nav-item">
      <a class="nav-link active" href="https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/extras/conv.md">Suggest edits to this page on GitHub</a>
    </li>
  </ul>
</nav>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>